0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 85 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 0 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 25 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 PiDP
↳9 UsableRulesProof (⇔, 0 ms)
↳10 PiDP
↳11 PiDPToQDPProof (⇒, 18 ms)
↳12 QDP
↳13 UsableRulesReductionPairsProof (⇔, 127 ms)
↳14 QDP
↳15 PisEmptyProof (⇔, 0 ms)
↳16 YES
countstackA_in_ga(empty, 0) → countstackA_out_ga(empty, 0)
countstackA_in_ga(push(nil, empty), 0) → countstackA_out_ga(push(nil, empty), 0)
countstackA_in_ga(push(nil, push(nil, T16)), T18) → U1_ga(T16, T18, countstackA_in_ga(T16, T18))
countstackA_in_ga(push(nil, push(cons(T35, T36), T37)), s(T39)) → U2_ga(T35, T36, T37, T39, countstackA_in_ga(push(T35, push(T36, T37)), T39))
countstackA_in_ga(push(cons(nil, T61), T62), s(T64)) → U3_ga(T61, T62, T64, countstackA_in_ga(push(T61, T62), T64))
countstackA_in_ga(push(cons(cons(T75, T76), T77), T78), s(s(T80))) → U4_ga(T75, T76, T77, T78, T80, countstackA_in_ga(push(T75, push(T76, push(T77, T78))), T80))
U4_ga(T75, T76, T77, T78, T80, countstackA_out_ga(push(T75, push(T76, push(T77, T78))), T80)) → countstackA_out_ga(push(cons(cons(T75, T76), T77), T78), s(s(T80)))
U3_ga(T61, T62, T64, countstackA_out_ga(push(T61, T62), T64)) → countstackA_out_ga(push(cons(nil, T61), T62), s(T64))
U2_ga(T35, T36, T37, T39, countstackA_out_ga(push(T35, push(T36, T37)), T39)) → countstackA_out_ga(push(nil, push(cons(T35, T36), T37)), s(T39))
U1_ga(T16, T18, countstackA_out_ga(T16, T18)) → countstackA_out_ga(push(nil, push(nil, T16)), T18)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
countstackA_in_ga(empty, 0) → countstackA_out_ga(empty, 0)
countstackA_in_ga(push(nil, empty), 0) → countstackA_out_ga(push(nil, empty), 0)
countstackA_in_ga(push(nil, push(nil, T16)), T18) → U1_ga(T16, T18, countstackA_in_ga(T16, T18))
countstackA_in_ga(push(nil, push(cons(T35, T36), T37)), s(T39)) → U2_ga(T35, T36, T37, T39, countstackA_in_ga(push(T35, push(T36, T37)), T39))
countstackA_in_ga(push(cons(nil, T61), T62), s(T64)) → U3_ga(T61, T62, T64, countstackA_in_ga(push(T61, T62), T64))
countstackA_in_ga(push(cons(cons(T75, T76), T77), T78), s(s(T80))) → U4_ga(T75, T76, T77, T78, T80, countstackA_in_ga(push(T75, push(T76, push(T77, T78))), T80))
U4_ga(T75, T76, T77, T78, T80, countstackA_out_ga(push(T75, push(T76, push(T77, T78))), T80)) → countstackA_out_ga(push(cons(cons(T75, T76), T77), T78), s(s(T80)))
U3_ga(T61, T62, T64, countstackA_out_ga(push(T61, T62), T64)) → countstackA_out_ga(push(cons(nil, T61), T62), s(T64))
U2_ga(T35, T36, T37, T39, countstackA_out_ga(push(T35, push(T36, T37)), T39)) → countstackA_out_ga(push(nil, push(cons(T35, T36), T37)), s(T39))
U1_ga(T16, T18, countstackA_out_ga(T16, T18)) → countstackA_out_ga(push(nil, push(nil, T16)), T18)
COUNTSTACKA_IN_GA(push(nil, push(nil, T16)), T18) → U1_GA(T16, T18, countstackA_in_ga(T16, T18))
COUNTSTACKA_IN_GA(push(nil, push(nil, T16)), T18) → COUNTSTACKA_IN_GA(T16, T18)
COUNTSTACKA_IN_GA(push(nil, push(cons(T35, T36), T37)), s(T39)) → U2_GA(T35, T36, T37, T39, countstackA_in_ga(push(T35, push(T36, T37)), T39))
COUNTSTACKA_IN_GA(push(nil, push(cons(T35, T36), T37)), s(T39)) → COUNTSTACKA_IN_GA(push(T35, push(T36, T37)), T39)
COUNTSTACKA_IN_GA(push(cons(nil, T61), T62), s(T64)) → U3_GA(T61, T62, T64, countstackA_in_ga(push(T61, T62), T64))
COUNTSTACKA_IN_GA(push(cons(nil, T61), T62), s(T64)) → COUNTSTACKA_IN_GA(push(T61, T62), T64)
COUNTSTACKA_IN_GA(push(cons(cons(T75, T76), T77), T78), s(s(T80))) → U4_GA(T75, T76, T77, T78, T80, countstackA_in_ga(push(T75, push(T76, push(T77, T78))), T80))
COUNTSTACKA_IN_GA(push(cons(cons(T75, T76), T77), T78), s(s(T80))) → COUNTSTACKA_IN_GA(push(T75, push(T76, push(T77, T78))), T80)
countstackA_in_ga(empty, 0) → countstackA_out_ga(empty, 0)
countstackA_in_ga(push(nil, empty), 0) → countstackA_out_ga(push(nil, empty), 0)
countstackA_in_ga(push(nil, push(nil, T16)), T18) → U1_ga(T16, T18, countstackA_in_ga(T16, T18))
countstackA_in_ga(push(nil, push(cons(T35, T36), T37)), s(T39)) → U2_ga(T35, T36, T37, T39, countstackA_in_ga(push(T35, push(T36, T37)), T39))
countstackA_in_ga(push(cons(nil, T61), T62), s(T64)) → U3_ga(T61, T62, T64, countstackA_in_ga(push(T61, T62), T64))
countstackA_in_ga(push(cons(cons(T75, T76), T77), T78), s(s(T80))) → U4_ga(T75, T76, T77, T78, T80, countstackA_in_ga(push(T75, push(T76, push(T77, T78))), T80))
U4_ga(T75, T76, T77, T78, T80, countstackA_out_ga(push(T75, push(T76, push(T77, T78))), T80)) → countstackA_out_ga(push(cons(cons(T75, T76), T77), T78), s(s(T80)))
U3_ga(T61, T62, T64, countstackA_out_ga(push(T61, T62), T64)) → countstackA_out_ga(push(cons(nil, T61), T62), s(T64))
U2_ga(T35, T36, T37, T39, countstackA_out_ga(push(T35, push(T36, T37)), T39)) → countstackA_out_ga(push(nil, push(cons(T35, T36), T37)), s(T39))
U1_ga(T16, T18, countstackA_out_ga(T16, T18)) → countstackA_out_ga(push(nil, push(nil, T16)), T18)
COUNTSTACKA_IN_GA(push(nil, push(nil, T16)), T18) → U1_GA(T16, T18, countstackA_in_ga(T16, T18))
COUNTSTACKA_IN_GA(push(nil, push(nil, T16)), T18) → COUNTSTACKA_IN_GA(T16, T18)
COUNTSTACKA_IN_GA(push(nil, push(cons(T35, T36), T37)), s(T39)) → U2_GA(T35, T36, T37, T39, countstackA_in_ga(push(T35, push(T36, T37)), T39))
COUNTSTACKA_IN_GA(push(nil, push(cons(T35, T36), T37)), s(T39)) → COUNTSTACKA_IN_GA(push(T35, push(T36, T37)), T39)
COUNTSTACKA_IN_GA(push(cons(nil, T61), T62), s(T64)) → U3_GA(T61, T62, T64, countstackA_in_ga(push(T61, T62), T64))
COUNTSTACKA_IN_GA(push(cons(nil, T61), T62), s(T64)) → COUNTSTACKA_IN_GA(push(T61, T62), T64)
COUNTSTACKA_IN_GA(push(cons(cons(T75, T76), T77), T78), s(s(T80))) → U4_GA(T75, T76, T77, T78, T80, countstackA_in_ga(push(T75, push(T76, push(T77, T78))), T80))
COUNTSTACKA_IN_GA(push(cons(cons(T75, T76), T77), T78), s(s(T80))) → COUNTSTACKA_IN_GA(push(T75, push(T76, push(T77, T78))), T80)
countstackA_in_ga(empty, 0) → countstackA_out_ga(empty, 0)
countstackA_in_ga(push(nil, empty), 0) → countstackA_out_ga(push(nil, empty), 0)
countstackA_in_ga(push(nil, push(nil, T16)), T18) → U1_ga(T16, T18, countstackA_in_ga(T16, T18))
countstackA_in_ga(push(nil, push(cons(T35, T36), T37)), s(T39)) → U2_ga(T35, T36, T37, T39, countstackA_in_ga(push(T35, push(T36, T37)), T39))
countstackA_in_ga(push(cons(nil, T61), T62), s(T64)) → U3_ga(T61, T62, T64, countstackA_in_ga(push(T61, T62), T64))
countstackA_in_ga(push(cons(cons(T75, T76), T77), T78), s(s(T80))) → U4_ga(T75, T76, T77, T78, T80, countstackA_in_ga(push(T75, push(T76, push(T77, T78))), T80))
U4_ga(T75, T76, T77, T78, T80, countstackA_out_ga(push(T75, push(T76, push(T77, T78))), T80)) → countstackA_out_ga(push(cons(cons(T75, T76), T77), T78), s(s(T80)))
U3_ga(T61, T62, T64, countstackA_out_ga(push(T61, T62), T64)) → countstackA_out_ga(push(cons(nil, T61), T62), s(T64))
U2_ga(T35, T36, T37, T39, countstackA_out_ga(push(T35, push(T36, T37)), T39)) → countstackA_out_ga(push(nil, push(cons(T35, T36), T37)), s(T39))
U1_ga(T16, T18, countstackA_out_ga(T16, T18)) → countstackA_out_ga(push(nil, push(nil, T16)), T18)
COUNTSTACKA_IN_GA(push(nil, push(cons(T35, T36), T37)), s(T39)) → COUNTSTACKA_IN_GA(push(T35, push(T36, T37)), T39)
COUNTSTACKA_IN_GA(push(nil, push(nil, T16)), T18) → COUNTSTACKA_IN_GA(T16, T18)
COUNTSTACKA_IN_GA(push(cons(nil, T61), T62), s(T64)) → COUNTSTACKA_IN_GA(push(T61, T62), T64)
COUNTSTACKA_IN_GA(push(cons(cons(T75, T76), T77), T78), s(s(T80))) → COUNTSTACKA_IN_GA(push(T75, push(T76, push(T77, T78))), T80)
countstackA_in_ga(empty, 0) → countstackA_out_ga(empty, 0)
countstackA_in_ga(push(nil, empty), 0) → countstackA_out_ga(push(nil, empty), 0)
countstackA_in_ga(push(nil, push(nil, T16)), T18) → U1_ga(T16, T18, countstackA_in_ga(T16, T18))
countstackA_in_ga(push(nil, push(cons(T35, T36), T37)), s(T39)) → U2_ga(T35, T36, T37, T39, countstackA_in_ga(push(T35, push(T36, T37)), T39))
countstackA_in_ga(push(cons(nil, T61), T62), s(T64)) → U3_ga(T61, T62, T64, countstackA_in_ga(push(T61, T62), T64))
countstackA_in_ga(push(cons(cons(T75, T76), T77), T78), s(s(T80))) → U4_ga(T75, T76, T77, T78, T80, countstackA_in_ga(push(T75, push(T76, push(T77, T78))), T80))
U4_ga(T75, T76, T77, T78, T80, countstackA_out_ga(push(T75, push(T76, push(T77, T78))), T80)) → countstackA_out_ga(push(cons(cons(T75, T76), T77), T78), s(s(T80)))
U3_ga(T61, T62, T64, countstackA_out_ga(push(T61, T62), T64)) → countstackA_out_ga(push(cons(nil, T61), T62), s(T64))
U2_ga(T35, T36, T37, T39, countstackA_out_ga(push(T35, push(T36, T37)), T39)) → countstackA_out_ga(push(nil, push(cons(T35, T36), T37)), s(T39))
U1_ga(T16, T18, countstackA_out_ga(T16, T18)) → countstackA_out_ga(push(nil, push(nil, T16)), T18)
COUNTSTACKA_IN_GA(push(nil, push(cons(T35, T36), T37)), s(T39)) → COUNTSTACKA_IN_GA(push(T35, push(T36, T37)), T39)
COUNTSTACKA_IN_GA(push(nil, push(nil, T16)), T18) → COUNTSTACKA_IN_GA(T16, T18)
COUNTSTACKA_IN_GA(push(cons(nil, T61), T62), s(T64)) → COUNTSTACKA_IN_GA(push(T61, T62), T64)
COUNTSTACKA_IN_GA(push(cons(cons(T75, T76), T77), T78), s(s(T80))) → COUNTSTACKA_IN_GA(push(T75, push(T76, push(T77, T78))), T80)
COUNTSTACKA_IN_GA(push(nil, push(cons(T35, T36), T37))) → COUNTSTACKA_IN_GA(push(T35, push(T36, T37)))
COUNTSTACKA_IN_GA(push(nil, push(nil, T16))) → COUNTSTACKA_IN_GA(T16)
COUNTSTACKA_IN_GA(push(cons(nil, T61), T62)) → COUNTSTACKA_IN_GA(push(T61, T62))
COUNTSTACKA_IN_GA(push(cons(cons(T75, T76), T77), T78)) → COUNTSTACKA_IN_GA(push(T75, push(T76, push(T77, T78))))
No rules are removed from R.
COUNTSTACKA_IN_GA(push(nil, push(cons(T35, T36), T37))) → COUNTSTACKA_IN_GA(push(T35, push(T36, T37)))
COUNTSTACKA_IN_GA(push(nil, push(nil, T16))) → COUNTSTACKA_IN_GA(T16)
COUNTSTACKA_IN_GA(push(cons(nil, T61), T62)) → COUNTSTACKA_IN_GA(push(T61, T62))
COUNTSTACKA_IN_GA(push(cons(cons(T75, T76), T77), T78)) → COUNTSTACKA_IN_GA(push(T75, push(T76, push(T77, T78))))
POL(COUNTSTACKA_IN_GA(x1)) = 2·x1
POL(cons(x1, x2)) = x1 + x2
POL(nil) = 0
POL(push(x1, x2)) = 2·x1 + x2